es:ES, p:(E(E + Top)).
causal-predecessor(es;p)  (e:E. (can-apply(p;e))  same-thread(es;p;e;do-apply(p;e))) 

latex

Definitions	SWellFounded(R(x;y)), f(a), p-graph(A;f), E, b, can-apply(f;x), suptype(S; T), S  T, x:A.B(x), Void, causal-predecessor(es;p), x:AB(x), left + right, Top, t  T, ES, same-thread(es;p;e;e'), x:A. B(x), P  Q, final-iterate(f;x), P  Q, s ~ t, SQType(T), {T}, P  Q, P & Q, x:A  B(x), A, s = t,
Lemmas	assert of bnot, eqff to assert, iff transitivity, bool sq, eqtt to assert, bool cases, causal-pred-wellfounded, event system wf, top wf, es-E wf, causal-predecessor wf, can-apply wf, assert wf